Termination w.r.t. Q of the following Term Rewriting System could be proven:
Q restricted rewrite system:
The TRS R consists of the following rules:
app2(app2(., 1), x) -> x
app2(app2(., x), 1) -> x
app2(app2(., app2(i, x)), x) -> 1
app2(app2(., x), app2(i, x)) -> 1
app2(app2(., app2(i, y)), app2(app2(., y), z)) -> z
app2(app2(., y), app2(app2(., app2(i, y)), z)) -> z
app2(i, 1) -> 1
app2(i, app2(i, x)) -> x
Q is empty.
↳ QTRS
↳ DependencyPairsProof
Q restricted rewrite system:
The TRS R consists of the following rules:
app2(app2(., 1), x) -> x
app2(app2(., x), 1) -> x
app2(app2(., app2(i, x)), x) -> 1
app2(app2(., x), app2(i, x)) -> 1
app2(app2(., app2(i, y)), app2(app2(., y), z)) -> z
app2(app2(., y), app2(app2(., app2(i, y)), z)) -> z
app2(i, 1) -> 1
app2(i, app2(i, x)) -> x
Q is empty.
Q DP problem:
P is empty.
The TRS R consists of the following rules:
app2(app2(., 1), x) -> x
app2(app2(., x), 1) -> x
app2(app2(., app2(i, x)), x) -> 1
app2(app2(., x), app2(i, x)) -> 1
app2(app2(., app2(i, y)), app2(app2(., y), z)) -> z
app2(app2(., y), app2(app2(., app2(i, y)), z)) -> z
app2(i, 1) -> 1
app2(i, app2(i, x)) -> x
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ PisEmptyProof
Q DP problem:
P is empty.
The TRS R consists of the following rules:
app2(app2(., 1), x) -> x
app2(app2(., x), 1) -> x
app2(app2(., app2(i, x)), x) -> 1
app2(app2(., x), app2(i, x)) -> 1
app2(app2(., app2(i, y)), app2(app2(., y), z)) -> z
app2(app2(., y), app2(app2(., app2(i, y)), z)) -> z
app2(i, 1) -> 1
app2(i, app2(i, x)) -> x
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.